Nuprl Lemma : generic_wf
0,22
postcript
pdf
T
:Type{i},
S
:((
T
)
Prop{i'}). generic{i:l}(
T
;
f
.
S
(
f
))
Prop{i'}
latex
Definitions
Type
,
t
T
,
Prop
,
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
||
as
||
,
P
&
Q
,
i
j
<
k
,
a
<
b
,
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
) }
,
{
i
..
j
}
,
#$n
,
Void
,
f
(
a
)
,
x
(
s
)
,
l
[
i
]
,
s
=
t
,
x
:
A
B
(
x
)
,
type
List
,
x
:
A
.
B
(
x
)
,
l1
l2
,
Generic{
f
:
T
|
S
(
f
)}
Lemmas
iseg
wf
,
int
seg
wf
,
select
wf
,
le
wf
,
length
wf1
,
nat
wf
origin
T:Type{i}, S:((
T)Prop{i'}). generic{i:l}(T; f.S(f)) 
Prop{i'} T:Type{i}, S:((T)Prop{i'}). generic{i:l}(T; f.S(f)) Prop{i'} TB(x)x:A. B(x)
j < k
Q
AB
}
B(x)
x:A. B(x) l2T|S(f)}